//
//  bmc.cpp
//  ltlbmc
//
//
//
#include <vector>
#include "tree.h"
#include "ast.h"
#include "bmc.h"


using namespace cilast;

bmc::bmc(file* cfile) {
    cfile = cfile;
    currlist = new std::vector<treeNode*>();
    todolist = new std::vector<treeNode*>();
    leaflist = new std::vector<treeNode*>();
}


void bmc::run(int maxUnroll, int maxRec) {
    this->maxUnroll = maxUnroll;
    this->maxRec = maxRec;
    
    //add start node
    treeNode* nEntry = (new treeNode())
    ->setRec(0)
    ->setUnroll(0)
    ->setPre(NULL)
    ->setCond(cfile->mainFundec->sbody->bstmts[0])
    ->setTarget(new satEX());
    currlist->push_back(nEntry);
    
    
    while(currlist->size()>0) {
        explore();
        
        if(isWitness()) {
            exit(0);
        }
        
        if(isStop()) {
            exit(0);
        }
    }

}

void bmc::explore() {
    
    
    
    
}


void bmc::push(treeNode* node) {
    if(node->unroll >= this->maxUnroll ||
       node->rec >= this->maxRec)
        leaflist->push_back(node);
    else
        todolist->push_back(node);

}

treeNode* bmc::pop() {
    treeNode* result = currlist->back();
    currlist->pop_back();
    return result;
}

void bmc::swap() {
    currlist->swap(*todolist);
}


bool bmc::isWitness() {
    
}

bool bmc::isStop() {
    
}


